\begin{tabbing}
($e$.$P$($e$) $\rightarrow$$a$.$f$($a$)$\rightarrow$ ${\it e'}$.$Q$(${\it e'}$)) with $R$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Bij(\{$e$:E$\mid$ $P$($e$)\} ;\{${\it e'}$:E$\mid$ $Q$(${\it e'}$)\} ;$\lambda$$a$.$f$($a$))\+
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ $P$($e$)\} . $e$ c$\leq$ $f$($e$) \& $R$(val($e$),val($f$($e$))))
\-
\end{tabbing}